Nuprl Lemma : sum_wf
11,40
postcript
pdf
n
:
,
f
:({0..
n
}
). sum(
f
(
x
) |
x
<
n
)
latex
Definitions
x
(
s
)
,
sum(
f
(
x
) |
x
<
k
)
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
,
int
seg
wf
,
primrec
wf
origin
n:
, f:({0..n
}
). sum(f(x) | x < n) 
n:, f:({0..n}). sum(f(x) | x < n) Tx:A. B(x)